<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>StepUnifier</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="StepUnifier";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/StepSelectorStore.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/UnifySubst.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/StepUnifier.html" target="_top">Frames</a></li>
<li><a href="StepUnifier.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.pa</div>
<h2 title="Class StepUnifier" class="title">Class StepUnifier</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.pa.StepUnifier</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">StepUnifier</span>
extends java.lang.Object</pre>
<div class="block">StepUnifier implements an algorithm based on Robinson's original unification
 algorithm to unify two formulas.
 <p>
 It is customized for mmj2's needs as discussed in
 <code>mmj2/doc/StepUnifier.html</code>.
 <p>
 StepUnifier has much in common with the unification algorithm in
 ProofUnifier. These are the main differences:
 <ol>
 <li>It accumulates VarHyp substitution results into the new "paSubst" slot in
 mmj.lang.VarHyp instead of indirectly in the assrtSubst array.</li>
 <li>It uses Work Variables instead of Dummy Variables.</li>
 <li>SubstAnswer is a 2 dimensional array of UnifySubst in StepUnifier instead
 of a 3 dimensional array of ParseNode, as in ProofUnifier. The payload of
 SubstAnswer is a linked list instead of an array (for a variety of
 reasons...)</li>
 <li>The contents of SubstAnswer[i][j] are "raw", meaning that two elements of
 the [i][j] list may be inconsistent. This reduces the efficiency of the
 unification process but is an unavoidable result of the presence of Work Vars
 in Step Unifier -- there may be multiple substitutions targeting a single Var
 that are different but consistent, which is not the case in Proof Unifier
 (only one substitution is stored however, but a chain of related
 substitutions may be generated during "subunification" and these results are
 dependent upon the previously accum'd logical hypotheses... so, to make it
 simple, we just store the "raw" substitutions pre-accumulation/merging.)</li>
 <li>The backout process for reversing partial results during processing of
 the sorted logical hypothesis arrays is different. One thing it has in common
 with ProofUnifier's backout process is that it too relies on the fact that
 only ONE substitution to a VarHyp is made -- so backout out an assignment
 does not require restoring a previous substitution, but simply null-ing it
 out.</li>
 <li>No attempt is made to salvage the work produced by
 unifyAndMergeHypsUnsorted() as is done in ProofUnifier when going into
 unifyAndMergeHypsSorted(). "Salvage" would mean pre-loading substAnswer with
 the usable unification results from the unsorted hyp array unification
 attempt. This salvage op could be done, but given the way that users are
 expected to actually *use* work variables with the mmj2 Proof Assistant GUI
 screen, it is likely that no discernable performance improvement would be
 observed. So why do it here?
 </ol></div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#F_LEVEL_NBR">F_LEVEL_NBR</a></strong></code>
<div class="block">Proof Step Formula assigned number -1 while logical hypotheses have
 indexes 0 -> n.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/StepUnifier.html#StepUnifier(mmj.lang.WorkVarManager)">StepUnifier</a></strong>(<a href="../../mmj/lang/WorkVarManager.html" title="class in mmj.lang">WorkVarManager</a>&nbsp;workVarManager)</code>
<div class="block">Constructor for StepUnifier.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#backoutFLevelApplieds()">backoutFLevelApplieds</a></strong>()</code>
<div class="block">Backout Proof Step Formula applied substitutions.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#finalizeAndLoadAssrtSubst()">finalizeAndLoadAssrtSubst</a></strong>()</code>
<div class="block">Resolve chained substitutions into Work Variables and load the assrtSubst
 array with the substitutions generated by successful Unification.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#getDerivAssrtXRef()">getDerivAssrtXRef</a></strong>()</code>
<div class="block">Returns an int array of indexes that cross references to the unifying
 assertion logical hypothesis index.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#startProofWorksheet()">startProofWorksheet</a></strong>()</code>
<div class="block">Initialization for handling unification of an entire Proof Worksheet.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#unifyAndMergeHypsSorted(mmj.lang.LogHyp[], mmj.pa.ProofStepStmt[])">unifyAndMergeHypsSorted</a></strong>(<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;assrtLogHypArray,
                       <a href="../../mmj/pa/ProofStepStmt.html" title="class in mmj.pa">ProofStepStmt</a>[]&nbsp;derivStepHypArray)</code>
<div class="block">Unifies sorted proof step logical hypotheses against a sorted array of
 assertion logical hypotheses.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#unifyAndMergeHypsUnsorted(mmj.pa.ProofStepStmt[])">unifyAndMergeHypsUnsorted</a></strong>(<a href="../../mmj/pa/ProofStepStmt.html" title="class in mmj.pa">ProofStepStmt</a>[]&nbsp;derivStepHypArray)</code>
<div class="block">Unifies proof step logical hypotheses against an assertion's array of
 logical hypotheses.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/StepUnifier.html#unifyAndMergeStepFormula(boolean, mmj.lang.ParseNode, mmj.lang.ParseNode, mmj.lang.Hyp[], mmj.lang.LogHyp[])">unifyAndMergeStepFormula</a></strong>(boolean&nbsp;commit,
                        <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>&nbsp;assrtRoot,
                        <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>&nbsp;stepRoot,
                        <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;assrtHypArray,
                        <a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;assrtLogHypArray)</code>
<div class="block">Initialize for start of new Proof Step unification.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="F_LEVEL_NBR">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>F_LEVEL_NBR</h4>
<pre>public static&nbsp;int F_LEVEL_NBR</pre>
<div class="block">Proof Step Formula assigned number -1 while logical hypotheses have
 indexes 0 -> n.</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="StepUnifier(mmj.lang.WorkVarManager)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>StepUnifier</h4>
<pre>public&nbsp;StepUnifier(<a href="../../mmj/lang/WorkVarManager.html" title="class in mmj.lang">WorkVarManager</a>&nbsp;workVarManager)</pre>
<div class="block">Constructor for StepUnifier.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workVarManager</code> - instance of WorkVarManager.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="startProofWorksheet()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>startProofWorksheet</h4>
<pre>public&nbsp;void&nbsp;startProofWorksheet()</pre>
<div class="block">Initialization for handling unification of an entire Proof Worksheet.
 <p>
 NOTE: This function is vitally important -- it must be invoked at the
 start of Proof Worksheet processing in ProofUnifier.java (or whatever.)
 Its function is to prepare the Work Variables for use in the
 ProofWorksheet, including initializing their values and making sure that
 none are still allocated from previous usages. THEREFORE --</div>
</li>
</ul>
<a name="finalizeAndLoadAssrtSubst()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>finalizeAndLoadAssrtSubst</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;finalizeAndLoadAssrtSubst()</pre>
<div class="block">Resolve chained substitutions into Work Variables and load the assrtSubst
 array with the substitutions generated by successful Unification.
 <p>
 NOTE: This is an especially important part of the zany scheme to hold
 Work Variable substitution values inside the actual VarHyp instances
 (oy...) The resolution of chained substitutions into Work Variables does
 two vital things:
 <ol>
 <li>it eliminates multiple assignments, such as A = B, B = C, C = ( D ->
 E ), D = null, E = null, storing A = ( D -> E ), and B = ( D -> E ).
 <li>It *deallocates* A, B, and C!!! They get deallocated because after
 updating the Proof Worksheet with the Work Variable updates, A, B and C
 will no longer be present in the Proof Worksheet -- and!!! -- since
 deallocation does not erase any values, the assigned substitutions will
 be available during the time the Proof Worksheet is being updated... then
 when the next proof step is unified, A, B and C will be available for
 re-allocation, at which time their assigned values will be
 re-initialized.
 </ol>
 NOTE ALSO that because A, B and C are deallocated but still have
 instances in use inside the Proof Worksheet, the Proof Worksheet code can
 interrogate work variables it has in hand, and if one is *now* marked
 "deallocated" then it knows, for absolute fact, that that variable is
 being updated and removed! So, if proof step 3 uses work var "A" and work
 var "A" is marked as deallocated, then the program *knows* that it must
 update proof step 3's formula and parse tree, and that maybe proof step 3
 no longer has any work variables (or not...)</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>the substituted list of ParseNodes</dd></dl>
</li>
</ul>
<a name="getDerivAssrtXRef()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getDerivAssrtXRef</h4>
<pre>public&nbsp;int[]&nbsp;getDerivAssrtXRef()</pre>
<div class="block">Returns an int array of indexes that cross references to the unifying
 assertion logical hypothesis index.
 <p>
 Note that derivAssrtXRef index numbers correspond to the sorted arrays of
 Logical Hypotheses input to unifyAndMergeHypsSorted(). For example, if
 derivAssrtXRef[0] = 2 that means that the first (sorted) element of
 derivStepHypArray unifies with the 3rd (sorted) element of
 assrtLogHypArray.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>derivAssrtXRef array of int indexes.</dd></dl>
</li>
</ul>
<a name="backoutFLevelApplieds()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>backoutFLevelApplieds</h4>
<pre>public&nbsp;void&nbsp;backoutFLevelApplieds()</pre>
<div class="block">Backout Proof Step Formula applied substitutions.
 <p>
 This function would need to be used if the full sequence of calls is not
 performed:
 <ol>
 <li>unifyAndMergeStepFormula()</li>
 <li>unifyAndMergeHypsUnsorted()</li>
 <li>unifyAndMergeHypsSorted()</li>
 </ol>
 <p>
 If unification succeeds for (1) but (2) and (3) are not called, or, if
 (1) succeeds and (2) fails, but (3) is not called, then
 backoutFLevelApplieds() would be necessary to tidy up...
 <p>
 But, in normal ProofUnifier processing this function is not needed
 because it does perform the full sequence of calls.</div>
</li>
</ul>
<a name="unifyAndMergeStepFormula(boolean, mmj.lang.ParseNode, mmj.lang.ParseNode, mmj.lang.Hyp[], mmj.lang.LogHyp[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>unifyAndMergeStepFormula</h4>
<pre>public&nbsp;boolean&nbsp;unifyAndMergeStepFormula(boolean&nbsp;commit,
                               <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>&nbsp;assrtRoot,
                               <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>&nbsp;stepRoot,
                               <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;assrtHypArray,
                               <a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;assrtLogHypArray)
                                 throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Initialize for start of new Proof Step unification.
 <p>
 Then unify/merge the proof step formula but not, yet, the logical
 hypotheses.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>commit</code> - see <a href="../../mmj/pa/StepUnifier.html#commit"><code>commit</code></a></dd><dd><code>assrtRoot</code> - the root of the Assrt ParseTree</dd><dd><code>stepRoot</code> - the root of the step's formula ParseTree</dd><dd><code>assrtHypArray</code> - the mandatory hypArray</dd><dd><code>assrtLogHypArray</code> - the logHypArray</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if the proof step formula unifies with the input assertion's
         formula; otherwise false.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if an error occurs</dd></dl>
</li>
</ul>
<a name="unifyAndMergeHypsUnsorted(mmj.pa.ProofStepStmt[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>unifyAndMergeHypsUnsorted</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;unifyAndMergeHypsUnsorted(<a href="../../mmj/pa/ProofStepStmt.html" title="class in mmj.pa">ProofStepStmt</a>[]&nbsp;derivStepHypArray)</pre>
<div class="block">Unifies proof step logical hypotheses against an assertion's array of
 logical hypotheses.
 <p>
 The derivation step hypothesis order used ought to be the order input by
 the user -- only if that order is wrong should unifyAndMergeHypsSorted()
 be used.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>derivStepHypArray</code> - the hypArray for the derivation step</dd>
<dt><span class="strong">Returns:</span></dt><dd>array assrtSubst, a ParseNode array parallel to
         assrt.MandFrame.hyp.</dd></dl>
</li>
</ul>
<a name="unifyAndMergeHypsSorted(mmj.lang.LogHyp[], mmj.pa.ProofStepStmt[])">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>unifyAndMergeHypsSorted</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;unifyAndMergeHypsSorted(<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;assrtLogHypArray,
                                  <a href="../../mmj/pa/ProofStepStmt.html" title="class in mmj.pa">ProofStepStmt</a>[]&nbsp;derivStepHypArray)</pre>
<div class="block">Unifies sorted proof step logical hypotheses against a sorted array of
 assertion logical hypotheses.
 <p>
 This function ought to be called after first attempting
 unifyAndMergeHypsUnsorted() because the user's hypothesis order may be
 significant: there can be more than one valid, consistent unification if
 work variables are present in a proof step and its hypotheses. Therefore,
 this function ought to be used as a last resort (especially since it is
 slow.....)
 <p>
 The sort order of the input assrtLogHypArray and derivStepHypArray is
 particularly important due to the potential problem of combinatorial
 explosion requiring n-factorial hypothesis-pair unification attempts if
 the sort order is precisely wrong :-) ProofUnifier uses
 sortAssrtLogHypArray() and sortDerivStepHypArray() to order the
 hypotheses in order by descending formula length -- and if two formulas
 have equal length, then if one has a variable in common with the
 derivation step's main formula, then that hypothesis is placed ahead of
 the other. This sort order is based on empirical observation -- and seems
 to work ok.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>assrtLogHypArray</code> - the logHypArray</dd><dd><code>derivStepHypArray</code> - the hypArray for the derivation step</dd>
<dt><span class="strong">Returns:</span></dt><dd>array assrtSubst, a ParseNode array parallel to
         assrt.MandFrame.hyp.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/StepSelectorStore.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/UnifySubst.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/StepUnifier.html" target="_top">Frames</a></li>
<li><a href="StepUnifier.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
